the_es:ES, j, e:E. first(j)  (e <loc j) 

latex

Definitions	t  T, x:A. B(x), P  Q, P & Q, P  Q, E, first(e), b, (e <loc e'), False, A, ES
Lemmas	event system wf, es-axioms, assert wf, es-first wf, es-E wf